A:Type, eq:EqDecider(A), x:A, v, z, f:Top. x : v  f(x)?z ~ v 

latex

Definitions	<a,b>, x:A. B(x), t  T, {T}, P  Q, SQType(T), Prop, s ~ t, left+right, f(x), x  dom(f), f(x)?z, f  g, x : v, Type, EqDecider(T), Top, true, eqof(d), f(a), , s = t, P & Q, P  Q, False, A, false, b, b, x:AB(x), x:AB(x), Unit
Lemmas	eqtt to assert, iff transitivity, eqff to assert, assert of bnot, bnot wf, not wf, assert wf, top wf, deq wf, bool wf, bool sq, eqof wf, btrue wf